$\forall$$D$:Dsys, ${\it rx}$, ${\it ra}$, ${\it rt}$:(Id$\rightarrow$Id).
\\[0ex]Inj(Id; Id; ${\it rx}$) $\Rightarrow$ Inj(Id; Id; ${\it ra}$) $\Rightarrow$ Inj(Id; Id; ${\it rt}$) $\Rightarrow$ d{-}rename(${\it rx}$;${\it ra}$;${\it rt}$;$D$) $\in$ Dsys